﻿using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using System.Threading.Tasks;

namespace OverSATbLib
{
    public class CNFSatSolver
    {
        public static string  SolveCNFString( string cnfStringText, int maximumResults )
        {
            StringBuilder results = new StringBuilder();
            var solver = CreateSATSolver(cnfStringText);
            var solutionList = solver.GetTrueValues(maximumResults);
            results.AppendFormat("c OverSATb {0} solutions" + Environment.NewLine, solutionList.Count);
            results.AppendFormat("s cnf {0} {1} {2}" + Environment.NewLine, (solutionList.Count > 0 ? 1 : 0), solver.VariablesUsed.Count, solver.ClausesUsed);
            foreach (var solution in solutionList)
            {
                results.AppendFormat("v {0} 0" + Environment.NewLine, string.Join(" ", solution.AssignItems.Select(a => ((a.Value > 0) ? a.NameId : -a.NameId).ToString()).ToArray()));
            }
            return results.ToString();
        }

        public static SatSolver CreateSATSolver(string cnfStringText)
        {
            string tabsToSpace = cnfStringText.Replace('\t', ' ');
            string cleanSigns = tabsToSpace.Replace("- ", "-");
            string escapedText = cleanSigns.Replace("\r\n", "\n");

            string[] cnfStringLines = escapedText.Split('\n');

            List<int> currentClause = new List<int>();
            SatSolver solver = new SatSolver();
            for (int i = 0; i < cnfStringLines.Length; i++)
            {
                string line = cnfStringLines[i];
                if (line.Length > 0)
                {
                    string[] words = line.Split(' ')
                                    .ToArray();

                    switch (line[0])
                    {
                        case 'c': // comment line, ignore
                            break;

                        case 'p': // problem line. 
                            {
                                if (words[1] != "cnf")
                                {
                                    throw new ArgumentException(string.Format("Input set must be of form 'p cnf', but 'p {0}' was given.", words[1]));
                                }
                            }
                            break;

                        default:
                            {
                                int[] numbers = words
                                    .Where(a => !string.IsNullOrEmpty(a))
                                    .Select(a => int.Parse(a)).ToArray();
                                for (int j = 0; j < numbers.Length; j++)
                                {
                                    int n = numbers[j];
                                    if (n == 0)
                                    {
                                        solver.AddClause(currentClause);
                                        currentClause.Clear();
                                    }
                                    else
                                    {
                                        currentClause.Add(n);
                                    }
                                }
                            }
                            break;
                    }
                }
            }
            solver.Optimize();

            if (currentClause.Count > 0)
            {
                solver.AddClause(currentClause);
                currentClause.Clear();
            }

            return solver;
        }
    }
}
